M1, M2:MsgA, x:Id. M1  M2  M2.ds(x)  M1.ds(x) 

latex

Definitions	M.ds(x), M1  M2, MsgA, Valtype(da;k), A & B, P & Q, x:A. B(x), P  Q, Top, Id, IdDeq, t  T
Lemmas	id-deq wf, Id wf, top wf, subtype-fpf-cap-top, msga wf, ma-sub wf